【第1814期】函数式编程起源-Lambda演算(es2015描述)

前言

今日早读文章由酷家乐@Gloria翻译投稿分享。

正文从这开始～～

判定性问题和可计算性：

在形式化语言中，如何有效地接收并且验证一个命题的正确性？

简单来说，这是早在1928年提出的一个重要的数学问题：“判定性问题” （decision problem）。在数年之后的1936年，Alonzo Church 和 Alan Turing 证明了：为“判定性问题”设计一个通用算法这件事是不可能的。

与此同时，他们各自详细阐述了两个计算模型：Alonzo Church的Lambda演算（后文都称λ演算），Alan Turing的理论机器（之后被称作图灵机）。

冯.诺依曼结构实现了理论上的图灵机，并且用在了如今的电脑上。而Alonzo Church的计算模型，其实与图灵机一样强大，但由于一些历史原因，走了上了一条更加学术化，更不商业化的道路。

本文会借助javascript的语法（es2015）来介绍λ演算中的一些重要概念，展现λ演算对现代语言的影响和对未来编程的重要性。

Lambda演算

λ演算是一个为了表达和计算函数的形式化系统，有着自己的化简规则和语法。整个系统是基于表达式的（也叫λ项）。

一个表达式可以是一个变量（variable），一个抽象体（abstraction）或者一个应用（application）。

1. expression = variable || abstraction || application

下面是所有的表达式类型：

变量 X 就是一个表达式

1. variable = expression

如果 X 是变量，E 是表达式，则λx.E是一个抽象体

1. abstraction = λ(variable).(expression)

如果 E 和 A 都是表达式，则 EA 是一个应用

1. application = (expression)(expression)

函数抽象体

在λ演算中，函数是用λ表示的匿名函数。一个匿名函数中只存在标识符和他自己的函数体。下面的表达式定义了一个函数（也叫做λ抽象体）：

紧跟在λ后面的名字是参数标识符，点（.）后面的表达式是函数体。我们用javascript表示它：

1. function(x) {

2. return x

3. }

改写成箭头函数：

1. x => x

现在定义一个抽象体，它接收一个变量y，然后返回y的平方，我们可以这么写：

函数应用

函数可以被应用在表达式上。在表达式 EA 中，E 是一个函数，它被应用到了表达式 A 上。换句话来说，表达式 A 就是表达式 E 的输入，然后输出 E(A) 。

把 E 替换成抽象体 λy.y^2，然后得到下面的式子：

1. const E = y => (y ** 2) // Abstraction

2. E(A) // Application

通过将函数体中的 y 替换成参数 y 的值，来计算这个函数应用的结果。比如：把表达式 A 替换成整数“5”：

y[y:=A]意思是：在函数体中，所有出现变量 y 的地方必须都被替换成表达式 A 。

多参函数

λ 演算中的所有抽象体都只接收一个参数。如果要实现获取多个参数，就要借助多重应用了。如果有下面这样的函数：

我们其实习惯像下面这样定义和应用它：

1. const F = (x,y) => (x + y)

2. F(5, 10)

用不同的方式，我们可以先定义一个函数，这个函数接收一个参数 x ，返回一个新的函数，这个新的函数接收一个参数 y ：

1. const F = x => (y => (x + y))

可以通过下面两步，应用这个接收两个参数的函数：

1. const F = x => (y => (x + y))

2. F(5)(10)

3. // "x => (y => 5 + y)"

4. // "x => (y => 5 + 10)"

5. // 15

这个策略就是传说中的“柯里化”（Currying），在Haskell Curry中有介绍。

为了便于理解，想象一个计算矩形面积（A=base * height）的抽象体：

1. constRectangleArea= base=> (height => (base* height))

2. RectangleArea(2)(4)

将 2 传进第一个函数的参数 base ，然后返回一个新的函数。将 4 传进第二个函数，作为 height 的值，最终返回这个矩形的面积。

定义数据类型

在无类型λ演算中，函数是唯一的基础类型。所以，如果要使用布尔类型，数字类型以及算数运算，就需要定义一些抽象体去表示它们。接下来我们定义一些比较简单的类型及它们的运算：布尔类型，and 与 or 操作。

如果你想深入了解，推荐看一看 The untyped Lambda Calculus

Alonzo Church 这样定义布尔类型：

1. constTrue= a => b => a

2. constFalse= a => b => b

可以把布尔值的逻辑运算看作是一种“抉择行为”。上面两个函数中，都有2个参数，最终返回其中一个参数。不同的是，函数 True 选择返回第一个参数，而函数 False 选择返回第二个。

基于上面的定义，可以得出 If-then-else 的结构：

1. constIf= Condition=> Then=> Else=> Condition(Then)(Else)

如果 Condition 的位置接收到的是 True ，那么就会返回 Then 作为结果，因为 True 总是返回第一个参数。如果 Condition 的位置接收到的是 False ，那么就会返回 Else 作为结果，因为 False 总是返回第二个参数。

定义下面两个log函数，帮助我们查看运行结果

1. const isTrue = () => "it's true!"

2. const isFalse = () => "it's false!"

将布尔值传进 If ：

1. constFirst= If(True)(isTrue)(isFalse)

2. constSecond= If(False)(isTrue)(isFalse)

3. First() // "it's true!"

4. Second() // "it's false!"

现在我们通过化简的过程解释这个结果。我们可以发现 a 其实就是 Then ， b 就是 Else ：

在了解了 If 的定义之后，再看看 and 和 or 的定义：

1. constAnd= Exp1=> Exp2=> Exp1(Exp2)(Exp1)

2. constOr= Exp1=> Exp2=> Exp1(Exp1)(Exp2)

在数学逻辑运算中，只有当两个表达式都是 true 的时候， and 操作符才会返回 true 。or 操作符只有当两个表达式都是 false 的时候，才会返回 false 。基于上面的结论，函数 And 始终会返回 False ，除非 And(True)(True) 这样调用它。函数 Or 始终会返回 True ，除非 Or(False)(False) 这样调用它。

只需要通过置换操作符应用中的变量，就能检验上面所定义的式子。比如像下面这样：

下面是所有可能的化简过程：

1. | Operator| Reduction| Result|

2. |-------------------|---------------------|-----------|

3. | And(True)(True) | True(True)(True) | True|

4. | And(True)(False) | True(False)(True) | False|

5. | And(False)(True) | False(True)(False) | False|

6. | And(False)(False) | False(False)(False) | False|

7. | Or(True)(True) | True(True)(True) | True|

8. | Or(True)(False) | True(True)(False) | True|

9. | Or(False)(True) | False(False)(True) | True|

10. | Or(False)(False) | False(False)(False) | False|

到目前为止，我们已经定义了很多结构，如：True ， False ， If ， And ， Or ，接下来通过比较简单和直观的方式检验一下：

1. constResult1= If(And(True)(True))(isTrue)(isFalse)

2. constResult2= If(And(True)(False))(isTrue)(isFalse)

3. constResult3= If(Or(False)(True))(isTrue)(isFalse)

4. constResult4= If(Or(False)(False))(isTrue)(isFalse)

5. Result1() // "it's true"

6. Result2() // "it's false"

7. Result3() // "it's true"

8. Result4() // "it's false"

最后，你需要记住的是，λ演算并不是数据类型的具体实现，只是一个形式化的系统，它并不需要代表任何计算过程，因为都可以使用函数去模拟它们。

λ演算和函数式编程

通过图灵机描述的可计算性，引出了命令式编程。通过λ演算描述的可计算性，引出了函数式编程 -- Cooper & Leeuwen（2013）

早在电子计算机诞生之前，Alonzo Church 就创造了λ演算。但它对现代编程语言却有着深远的影响。作为第二个高级编程语言的Lisp，它就是启发自λ演算。再比如说，所有支持匿名函数的语言里（像Haskell，JavaScript，Python，Ruby等等）都会有几分Alonzo Church的影子。

函数式的模式催生表达能力强的代码，因为这些模式与数学模型有着更加直接的对应关系，因此也更加合理。正因为在数学的世界里，函数式的代码具备引用透明性（给定相同的输入，始终会有相同的输出），这让它可以在多个处理器中同时运行。

λ演算影响着多种多样的现代编程语言，这不仅仅是因为它的形式化系统是图灵完备的，也是因为它的简洁性和表达能力，这些层面上的能力是对未来的编程是非常重要的。

参考资料

• Henk Barendregt, Erik Barendsen (2000). Introduction to Lambda Calculus.

• Raúl Rojas (1998). A Tutorial Introduction to the Lambda Calculus.

• Manuel Eberl (2011). The untyped Lambda Calculus.

• Barry Cooper, J. van Leeuwen (2013). Alan Turing: His Work and Impact .

关于本文 译者：@Gloria 译文：https://zhuanlan.zhihu.com/p/98104104 作者：@Alexandre Thebaldi 原文：https://medium.com/@ahlechandre/lambda-calculus-with-javascript-897f7e81f259

为你推荐